\begin{tabbing}
$\forall$\=$A$:Type, $B$:($A$$\rightarrow$Type), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$), ${\it eq}$:EqDecider($A$), $x$:$A$,\+
\\[0ex]$P$:($a$:\{$a$:$A$$\mid$ $a$ $\in$ dom($f$) \}$\rightarrow$$B$($a$)$\rightarrow$Prop).
\-\\[0ex]($z$ != $f$($x$) $\Rightarrow$ $P$($x$,$z$)) $\in$ Prop
\end{tabbing}